Nuprl Lemma : comb_for_member_wf
13,42
postcript
pdf
(
A
,
a
,
z
.
a
A
)
A
:Type
A
(
True)
Type
latex
Up
core
2
,
core
2
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
Lemmas
true
wf
,
squash
wf
,
member
wf
origin
A,a,z. a 
A) A:Type
A(
True)Type A,a,z. a A) A:TypeA(True)Type T
x:A. B(x)T